\begin{tabbing}
$\forall$\=$A$:Type, ${\it none}$:$A$, ${\it comb}$:($A$$\rightarrow$$A$$\rightarrow$$A$),\+
\\[0ex]${\it base}$:(\{$R$:Realizer$\mid$ ($\neg$($\uparrow$Rnone?($R$))) \& ($\neg$($\uparrow$Rplus?($R$)))\} $\rightarrow$$A$), $R$:Realizer.
\-\\[0ex]case($R$)Rnone: ${\it none}$${\it left}$ $\oplus$ ${\it right}$: ${\it comb}$(${\it left}$,${\it right}$)base($b$). ${\it base}$($b$) $\in$ $A$
\end{tabbing}